Nuprl Lemma : restriction-of-transitive
11,40
postcript
pdf
T
:Type,
R
:(
T
T
),
P
:(
T
). Trans(
T
;
x
,
y
.
R
(
x
,
y
))
Trans(
T
;
x
,
y
.
R
|
P
(
x
,
y
))
latex
Definitions
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
,
Type
,
P
Q
,
Trans(
T
;
x
,
y
.
E
(
x
;
y
))
,
f
(
a
)
,
R
|
P
,
P
&
Q
,
x
:
A
B
(
x
)
,
t
T
origin
T:Type, R:(T
T
), P:(T). Trans(T;x,y.R(x,y)) 
Trans(T;x,y.R|P(x,y)) T:Type, R:(TT), P:(T). Trans(T;x,y.R(x,y)) Trans(T;x,y.R|P(x,y)) x:A. B(x)B(x) Q
B(x)
T